\begin{tabbing}
$e$ $<$loc ${\it e'}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Case TERMOF\{decidable\_\_es{-}locl:ObjectId, 1:l, i:l\}(${\it es}$,${\it e'}$,$e$) of\+
\\[0ex]inl($x$) $\Rightarrow$ true$_{2}$
\\[0ex]inr($x$) $\Rightarrow$ false$_{2}$
\-
\end{tabbing}